nLab Initiality Project - Substitution

Initiality Project - Substitution

Initiality Project - Substitution

This page is part of the Initiality Project.

Statements

Based on the definition of the partial interpretation functions, we now prove the following substitution properties by mutual induction over raw terms and types.

Weakening, exchange, and contraction

Let V 1,V 2VarV_1,V_2 \subseteq Var be finite, and suppose θ:V 1V 2\theta : V_1\to V_2 is a function. Then:

  • For any raw type AA, the composite partial morphism Tm V 2Tm θTm V 1A type V 1TyTm^{V_2} \xrightarrow{Tm^\theta} Tm^{V_1} \overset{\⟦ A \⟧^{V_1}_{type}}\rightharpoonup Ty is contained in the partial morphism Tm V 2A[θ] type V 2TyTm^{V_2} \overset{\⟦ A[\theta] \⟧^{V_2}_{type}}\rightharpoonup Ty.
  • For any raw term TT, the composite partial morphism Tm V 2Tm θTm V 1T V 1TmTm^{V_2} \xrightarrow{Tm^\theta} Tm^{V_1} \overset{\⟦ T \⟧^{V_1}_{\Rightarrow}}\rightharpoonup Tm is contained in the partial morphism Tm V 2T[θ] V 2TmTm^{V_2} \overset{\⟦ T[\theta] \⟧^{V_2}_{\Rightarrow}}\rightharpoonup Tm.
  • For any raw term TT, the composite partial morphism Tm V 2×TyTm θTm V 1×TyT V 1TmTm^{V_2}\times Ty \xrightarrow{Tm^\theta} Tm^{V_1} \times Ty \overset{\⟦ T \⟧^{V_1}_{\Leftarrow}}\rightharpoonup Tm is contained in the partial morphism Tm V 2×TyT[θ] V 2TmTm^{V_2}\times Ty \overset{\⟦ T[\theta] \⟧^{V_2}_{\Leftarrow}}\rightharpoonup Tm.

Here A[θ]A[\theta] and T[θ]T[\theta] denote simultaneous capture-avoiding substitution of θ(x)\theta(x) for each variable xV 1x\in V_1. When θ\theta is a bijection, this asserts invariance under renaming of free variables. When θ\theta is an inclusion, it asserts weakening, and when θ\theta is surjective it is contraction. Note that in general these containments can be strict, e.g. if some variable in V 2θ(V 1)V_2 \setminus \theta(V_1) appears freely in AA or TT, then the composites may have empty domain while the morphisms they are being compared to might not.

Substitution

Let VVarV\subseteq Var be finite and xVarVx\in Var\setminus V, while NN is a raw term. Then:

  • For any raw type AA, the composite partial morphism Tm V(id,N V)Tm V{x}A type V{x}TyTm^V \overset{(id,\⟦ N \⟧^V_{\Rightarrow})}{\rightharpoonup} Tm^{V\cup \{x\}} \overset{\⟦ A \⟧^{V\cup \{x\}}_{type}}{\rightharpoonup} Ty is contained in the partial morphism Tm VA[N/x] type VTyTm^V \overset{\⟦ A[N/x] \⟧^V_{type}}{\rightharpoonup} Ty.
  • For any raw term TT, the composite partial morphism Tm V(id,N V)Tm V{x}T V{x}TmTm^V \overset{(id,\⟦ N \⟧^V_{\Rightarrow})}{\rightharpoonup} Tm^{V\cup \{x\}} \overset{\⟦ T \⟧^{V\cup \{x\}}_{\Rightarrow}}{\rightharpoonup} Tm is contained in the partial morphism Tm VT[N/x] VTmTm^V \overset{\⟦ T[N/x] \⟧^V_{\Rightarrow}}{\rightharpoonup} Tm.
  • For any raw term TT, the composite partial morphism Tm V×Ty(id,N V,id)Tm V{x}×TyT V{x}TmTm^V\times Ty \overset{(id,\⟦ N \⟧^V_{\Rightarrow},id)}{\rightharpoonup} Tm^{V\cup \{x\}}\times Ty \overset{\⟦ T \⟧^{V\cup \{x\}}_{\Leftarrow}}{\rightharpoonup} Tm is contained in the partial morphism Tm V×TyT[N/x] VTmTm^V \times Ty\overset{\⟦ T[N/x] \⟧^V_{\Leftarrow}}{\rightharpoonup} Tm.

Inductive clauses

TODO.

Last revised on November 2, 2018 at 19:45:40. See the history of this page for a list of all contributions to it.